/**                   GNU GENERAL PUBLIC LICENSE
 *                       Version 3, 29 June 2007
 *
 * Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
 * Everyone is permitted to copy and distribute verbatim copies
 * of this license document, but changing it is not allowed.
 * See License.txt file that comes with this distribution
 *
 *
 * Author: Vitaly German <vitaly.german@gmail.com>, (C) 2007-2008
 * 
 **/

#pragma once


#ifdef DEBUG
 #define BOOST_SPIRIT_DUMP_PARSETREE_AS_XML
 #define BOOST_SPIRIT_DEBUG        // define this for debug output
#endif

//#define BOOST_SPIRIT_DEBUG_FLAGS
//#define BOOST_SPIRIT_DEBUG_FLAGS_NODES

#include <boost/spirit/core.hpp>
#include <boost/spirit/tree/ast.hpp>
#include <boost/spirit/tree/tree_to_xml.hpp>
#include <boost/spirit/utility/distinct.hpp>


#include <iostream>
#include <sstream>
#include <functional>

#include <boost/function.hpp>

#include "lr_fcalc_exceptions.hpp"
#include "inline_can.hpp"

using namespace boost::spirit;

// keyword_p for C++
// (for basic usage instead of std_p)
const distinct_parser<> keyword_p("0-9a-zA-Z_");

// keyword_d for C++
// (for mor intricate usage, for example together with symbol tables)
const distinct_directive<> keyword_d("0-9a-zA-Z_");

//////////////////////////////////////////////////////////////////////////////
/// The Solver Grammar
//////////////////////////////////////////////////////////////////////////////

struct calculator : public grammar<calculator> {
    static const int quantifierID = 1;
    static const int var_listID = 2;
    static const int variableID = 3;
    static const int logicID = 4;
    static const int logic1ID = 11;
    static const int logic2ID = 12;
    static const int ltermID = 5;
    static const int equsID = 6;
    static const int mathID = 7;
    static const int mexprID = 8;
    static const int factorID = 9;
    static const int realID = 10;


    template <typename ScannerT>
    struct definition {
        definition(calculator const& /*self*/) {
            quantifier 
                = access_node_d [
				  (
                   root_node_d
                   [
                      keyword_p("Forall")
                   ]

                | //
                         root_node_d[keyword_p("Exists")]
				     | root_node_d[keyword_p("Exist")]
				  //  
                )
				][logic_transform()]
                   >> var_list
                ;
            var_list 
                =   infix_node_d 
                    [
                       variable 
                       >> *(',' 
                       >> variable)
                     ] // TODO: Simplify
                |  inner_node_d 
                   [
                      ch_p('(') 
                      >> infix_node_d 
                         [
                            variable 
                            >> *(','>> variable)
                         ] 
                      >> ch_p(')')
                   ]
                ;
            variable 
                =   leaf_node_d [
                    lexeme_d 
                    [
                       alpha_p >> *(alnum_p | '_')
                    ]
                ];
            logic
                =   logic1
                    >> *(  
					    access_node_d
						[
							   
							  root_node_d[str_p("\\|")]
							| root_node_d[str_p("|/")]
							| root_node_d[str_p("||")]
							| root_node_d[str_p("\\/")]
							| root_node_d[str_p("or")]
							| root_node_d[ch_p('|')]
						] [logic_transform()] 
                        >> logic1
                    )
                ;
            logic1 
                =   logic2
                    >> *(
                        access_node_d
						[
							  root_node_d[str_p("&&")]
							| root_node_d[str_p("/\\")]
							| root_node_d[str_p("and")]
							| root_node_d[ch_p('&')]
						] [logic_transform()]
			          >> logic2
				    )
                ;
            logic2 
                =
                    !(root_node_d[ch_p('~')]) >> lterm
                ;

            lterm 
                =
                    access_node_d[equs][equs_transform()]
                |   quantifier >> 
                       logic
                |  
                   inner_node_d [
                      ch_p('(') >> 
                          (  quantifier >> logic
                            | logic)
                      >> ch_p(')')
                   ]
                ;
            equs 
                =   math
                    >> (   root_node_d[str_p(">=")]
                       |  root_node_d[str_p("<=")]
                       |  root_node_d[ch_p('>')]
                       |  root_node_d[ch_p('<')]
                       |  root_node_d[ch_p('=')]
                    )
                    >> math
                ;
            math 
                =   mexpr
                    >>  *( (root_node_d[ch_p('+')] >> mexpr)
                         |  (root_node_d[ch_p('-')] >> mexpr)
                         )
                ;
            mexpr 
                = factor
                   >>*((root_node_d[ch_p('*')] >> factor)
                   |  (root_node_d[ch_p('/')] >> factor)
                )
                ;
            factor 
                =   real
                |   variable
                |   inner_node_d [ch_p('(') >> math >> ch_p(')')]
                |   (root_node_d[ch_p('-')] >> factor)
                ;
            real =
                   leaf_node_d [real_p]
                ;

            // TODO: enabel comments
            //  comment
            //     =   +((comment_p("//") | comment_p("/*", "*/"))
            //         >> *space_p)
            //     ;

            BOOST_SPIRIT_DEBUG_RULE(logic);
            BOOST_SPIRIT_DEBUG_RULE(lterm);
            BOOST_SPIRIT_DEBUG_RULE(logic1);
            BOOST_SPIRIT_DEBUG_RULE(logic2);
            BOOST_SPIRIT_DEBUG_RULE(var_list);

            BOOST_SPIRIT_DEBUG_RULE(variable);
            BOOST_SPIRIT_DEBUG_RULE(quantifier);
            BOOST_SPIRIT_DEBUG_RULE(equs);

            BOOST_SPIRIT_DEBUG_RULE(math);
            BOOST_SPIRIT_DEBUG_RULE(mexpr);
            BOOST_SPIRIT_DEBUG_RULE(factor);
            BOOST_SPIRIT_DEBUG_RULE(real);
        }

        rule<ScannerT, parser_context<>, parser_tag<factorID> > factor;
        rule<ScannerT, parser_context<>, parser_tag<mexprID> > mexpr;
        rule<ScannerT, parser_context<>, parser_tag<mathID> > math;

        rule<ScannerT, parser_context<>, parser_tag<equsID> > equs;
        rule<ScannerT, parser_context<>, parser_tag<quantifierID> > quantifier;
        rule<ScannerT, parser_context<>, parser_tag<variableID> > variable;

        rule<ScannerT, parser_context<>, parser_tag<var_listID> > var_list;
        rule<ScannerT, parser_context<>, parser_tag<ltermID> > lterm;
        rule<ScannerT, parser_context<>, parser_tag<logicID> > logic;

        rule<ScannerT, parser_context<>, parser_tag<logic1ID> > logic1;
        rule<ScannerT, parser_context<>, parser_tag<logic2ID> > logic2;

        rule<ScannerT, parser_context<>, parser_tag<realID> > real;
        //    rule<ScannerT> comment;

        rule<ScannerT, parser_context<>, parser_tag<logicID> > const&
        start() const {
            return logic;
        }
    };

};

//////////////////////////////////////////////////////////////////////////////
/// Node Marks
//////////////////////////////////////////////////////////////////////////////


template <typename TID, typename T = std::string>
struct Mark {
    typedef T value_type;
    typedef Mark<TID, T> self;
    Mark():id(TID(size_t(0))) {}
    Mark(TID id1, const T & v):id(id1), mark(v) {}
    bool operator == (const self & mt ) const {
        return (id == mt.id && mark == mt.mark);
    }
    bool operator < (const self & mt ) const {
        return (id < mt.id || (id == mt.id ? mark < mt.mark: false));
    }
    friend std::ostream& operator<<(std::ostream&o, const Mark & m) {
#ifdef DEBUG
        o<<"Mark("<<m.id<<", "<<m.mark<<")";
#endif
        return o;
    }
    TID id;
    T mark;
};

typedef Mark<boost::spirit::parser_id> MarkT;

template <class T = MarkT>
class MarkManager {

    MarkManager():
            plus(calculator::mathID, typename T::value_type("+")),
            minus(calculator::mathID, typename T::value_type("-")),
            uminus(calculator::factorID, typename T::value_type("-")),
            mult(calculator::mexprID, typename T::value_type("*")),
            div(calculator::mexprID, typename T::value_type("/")),
            forall(calculator::quantifierID, typename T::value_type("Forall")),
            exists(calculator::quantifierID, typename T::value_type("Exists")),
            orl(calculator::logicID, typename T::value_type("|")),
            andl(calculator::logic1ID, typename T::value_type("&")),
            notl(calculator::logic2ID, typename T::value_type("~")),
            gr(calculator::equsID, typename T::value_type(">") ),
            greq(calculator::equsID, typename T::value_type(">=")),
            eq(calculator::equsID, typename T::value_type("=")),
            null(0, typename T::value_type()),

    lterm(calculator::ltermID, typename T::value_type()) {}

    MarkManager & operator = (const MarkManager &);
    MarkManager(const MarkManager & );
public:

    static MarkManager & instance() {
        static MarkManager obj;
        return obj;
    }

    const T plus;
    const T minus;
    const T uminus;
    const T mult;
    const T div;
    /// logic
    const T forall;
    const T exists;
    const T orl;
    const T andl;
    const T notl;
    /// equalities and ineaulities
    const T gr;
    const T greq;
    const T eq;
    const T null; // default or any mark

    /// grammar auxiliary
    const T lterm;
};

typedef MarkManager<> MarkManagerT;
